home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / transform_2.06.2 < prev    next >
Text File  |  1992-04-03  |  10KB  |  332 lines
  1. %%%
  2. %%% version 2.00.0
  3. %%%   initial version
  4. %%% version 2.00.3
  5. %%%   added "outtreq" and "pullout_constants"
  6. %%% version 2.00.4
  7. %%%   fixed input clause count when transforming equation
  8. %%% version 2.00.5
  9. %%%   optimized equality transform by ordering literals in transformed clauses
  10. %%% version 2.00.8
  11. %%%   added lexicographic path ordering
  12. %%% version 2.01.3
  13. %%%   moved print_eq_trans to eq_trans
  14. %%% version 2.01.4
  15. %%%   modified rewriting of equations according to David Plaisted's method
  16. %%% version 2.01.8
  17. %%%   added transformed form of all non-input equations before hyper-linking
  18. %%% version 2.02.0
  19. %%%   made the support and distance for pulled out equations the same as input
  20. %%% version 2.02.2
  21. %%%   asserted pulled out equations at beginning of session
  22. %%%   deleted pulled out form when rewriting asserted clause
  23. %%% version 2.02.5
  24. %%%   asserted equations along with pulled out forms at beginning of session
  25. %%%   asserted pulled out forms of equations at the beginning of each round
  26. %%% version 2.03.4
  27. %%%   printed axioms
  28. %%% version 2.04.2
  29. %%%   modified transform_equations_session and transform_equation_round include
  30. %%%     pulled out forms forms for input equations
  31. %%% version 2.04.3
  32. %%%   when pulling out equations, ordered pulled out form so that pulled out
  33. %%%     literals for the smaller side with respect to path order come first
  34. %%%   removed transitivity axiom
  35. %%% version 2.04.4
  36. %%%   no longer pull out equations at the beginning of rounds
  37. %%%   restored transitivity axiom
  38. %%% version 2.04.5
  39. %%%   added restricted_rewrite to control whether restricted or unrestricted
  40. %%%     rewriting of equations is used
  41. %%%   added equality_transform_by_round flag
  42. %%%   when pulling out equations, ordered pulled out form so that pulled out
  43. %%%     literals for the larger side with respect to path order come first
  44. %%% version 2.04.8
  45. %%%   improved efficiency of transform_equations_round
  46. %%% version 2.05.1
  47. %%%   fixed transform_equations_round so that it works when neither
  48. %%%     fixed_priority nor slidepriority is specified
  49. %%% version 2.05.2
  50. %%%   added clause splitting to transform_equations_round
  51. %%% version 2.05.3
  52. %%%   added support for Quintus Prolog
  53. %%% version 2.06.2
  54. %%%   added restricted_equality_transform
  55. %%%
  56.  
  57. %%% 
  58. %%% Eq_trans performs the equality transformation on a set of literals.
  59. %%% If the number of variables becomes too large, an error message is printed
  60. %%% and the equality transform is not performed (the set of literals is simply
  61. %%% returned).
  62. %%% 
  63.     eq_trans(Ls,Ls) :-
  64.       not(equality_transform),
  65.       !.
  66.     eq_trans(Ls1,Ls2) :-
  67.       eq_trans_1(Ls1,Ls2),
  68.       print_eq_trans(Ls1,Ls2),
  69.       !.
  70.     eq_trans_1([S=T],Ls) :-
  71.       orient_equation(S=T,S1=T1),
  72.       pullout_subterms([S1],Ss1),
  73.       pullout_subterms([T1],Ss2),
  74.       eq_trans_2(S1,Ss1,T1,Ss2,Ss3),
  75.       identical_delete_all_duplicates(Ss3,Ss4),
  76.       replace_subterms([S1=T1],Ss4,Ls1),
  77.       ((restricted_equality_transform(N1), length(Ls1,N2), N2=<N1) -> (
  78.         reverse(Ls1,Ls)
  79.       ); (
  80.         append(Ss1,Ss2,Ss5),
  81.         identical_delete_all_duplicates(Ss5,Ss6),
  82.         replace_subterms([S1=T1],Ss6,Ls2),
  83.         reverse(Ls2,Ls)
  84.       )),
  85.       vars_tail(Ls,V),
  86.       check_numbervars(V,
  87.         'Number of variables overflows in equality transform !'),
  88.       !.
  89.     eq_trans_1(Ls1,Ls2) :-
  90.       not(Ls1 = [S=T]),
  91.       pullout_subterms(Ls1,Ss1),
  92.       identical_delete_all_duplicates(Ss1,Ss2),
  93.       replace_subterms(Ls1,Ss2,Ls3),
  94.       vars_tail(Ls3,V),
  95.       check_numbervars(V,
  96.         'Number of variables overflows in equality transform !'),
  97.       sort_literals(Ls3,Ls2),
  98.       !.
  99.     eq_trans_1(Ls,Ls).
  100.     eq_trans_2(S1,Ss1,T1,Ss2,Ss3) :-
  101.       nonvar(S1),
  102.       check_pullout_constant(S1),
  103.       nonvar(T1),
  104.       check_pullout_constant(T1),
  105.       !,
  106.       append([S1|Ss1],[T1|Ss2],Ss3).
  107.     eq_trans_2(S1,Ss1,T1,Ss2,Ss3) :-
  108.       nonvar(S1),
  109.       check_pullout_constant(S1),
  110.       !,
  111.       append([S1|Ss1],Ss2,Ss3).
  112.     eq_trans_2(S1,Ss1,T1,Ss2,Ss3) :-
  113.       nonvar(T1),
  114.       check_pullout_constant(T1),
  115.       !,
  116.       append(Ss1,[T1|Ss2],Ss3).
  117.     eq_trans_2(S1,Ss1,T1,Ss2,Ss3) :-
  118.       append(Ss1,Ss2,Ss3).
  119.  
  120. %%% 
  121. %%% Eq_trans_np performs the equality transformation on a set of literals
  122. %%% without printing the transformation even if outtreq is asserted.
  123. %%% 
  124.     eq_trans_np(Ls,Ls) :-
  125.       not(equality_transform),
  126.       !.
  127.     eq_trans_np(Ls1,Ls2) :-
  128.       eq_trans_1(Ls1,Ls2),
  129.       !.
  130.  
  131. %%%
  132. %%% Pullout_subterms pulls out all appropriate subterms from a set of terms.
  133. %%%
  134.     pullout_subterms([L],[]) :-
  135.       atomic(L),
  136.       !.
  137.     pullout_subterms([L],[]) :-
  138.       var(L),
  139.       !.
  140.     pullout_subterms(Ls,Ss) :- pullout_subterms(Ls,Ls,Ss).
  141.     pullout_subterms(Ls1,[not L|Ls2],Ss) :-
  142.       !,
  143.       pullout_subterms_args(Ls1,L,Ss1),
  144.       pullout_subterms(Ls1,Ls2,Ss2),
  145.       append(Ss1,Ss2,Ss),
  146.       !.
  147.     pullout_subterms(Ls1,[L|Ls2],Ss) :-
  148.       pullout_subterms_args(Ls1,L,Ss1),
  149.       pullout_subterms(Ls1,Ls2,Ss2),
  150.       append(Ss1,Ss2,Ss),
  151.       !.
  152.     pullout_subterms(_,[],[]).
  153.     pullout_subterms_1(Ls1,[L|Ls2],[L|Ss]) :-
  154.       nonvar(L),
  155.       check_pullout_constant(L),
  156.       !,
  157.       pullout_subterms_args(Ls1,L,Ss1),
  158.       pullout_subterms_1(Ls1,Ls2,Ss2),
  159.       append(Ss1,Ss2,Ss),
  160.       !.
  161.     pullout_subterms_1(Ls1,[L|Ls2],Ss) :-
  162.       pullout_subterms_args(Ls1,L,Ss1),
  163.       pullout_subterms_1(Ls1,Ls2,Ss2),
  164.       append(Ss1,Ss2,Ss),
  165.       !.
  166.     pullout_subterms_1(_,[],[]).
  167.  
  168. %%%
  169. %%% Check_pullout_constant determines if a constant subterm should be pulled
  170. %%% out.
  171. %%%
  172.     check_pullout_constant(S) :-
  173.       not(atomic(S)),
  174.       !.
  175.     check_pullout_constant(_) :-
  176.       pullout_constants,
  177.       !.
  178.  
  179. %%%
  180. %%% Pullout_subterms_arg pulls out all appropriate subterms from the arguments
  181. %%% of a term.  
  182. %%%
  183.     pullout_subterms_args(Ls,T,Ss) :-
  184.       nonvar(T),
  185.       !,
  186.       T=..[_|As],
  187.       pullout_subterms_1(Ls,As,Ss),
  188.       !.
  189.     pullout_subterms_args(_,_,[]).
  190.  
  191. %%%
  192. %%% Replace_subterms replaces a list of subterms in a set of literals.
  193. %%%
  194.     replace_subterms(Ts,[],Ts).
  195.     replace_subterms(Ts1,[S|Ss],Ts2) :-
  196.       replace_subterm(Ts1,S,X,Ts3),
  197.       replace_subterm(Ss,S,X,Ss1),
  198.       replace_subterms([not S=X|Ts3],Ss1,Ts2),
  199.       !.
  200.  
  201. %%%
  202. %%% Replace_subterm replaces a subterm in a set of terms.
  203. %%%
  204.     replace_subterm([],_,_,[]).
  205.     replace_subterm([T|Ts1],S,X,[X|Ts2]) :-
  206.       T==S,
  207.       !,
  208.       replace_subterm(Ts1,S,X,Ts2).
  209.     replace_subterm([T1|Ts1],S,X,[T2|Ts2]) :-
  210.       replace_subterm_args(T1,S,X,T2),
  211.       replace_subterm(Ts1,S,X,Ts2).
  212.  
  213. %%%
  214. %%% Replace_subterm_args replaces a subterm in the arguments of a term.  If the
  215. %%% term has no arguments, the term is not modified.
  216. %%%
  217.     replace_subterm_args(T1,S,X,T2) :-
  218.       nonvar(T1),
  219.       !,
  220.       T1=..[F|As1],
  221.       replace_subterm(As1,S,X,As2),
  222.       T2=..[F|As2],
  223.       !.
  224.     replace_subterm_args(T,_,_,T).
  225.  
  226. %%%
  227. %%% Sort_literals sorts a set of literals into ascending order with respect to
  228. %%% recursive path ordering taking negative literals to be larger than positive
  229. %%% literals.  The order of equivalentl literals is unspecified.
  230. %%%
  231.     sort_literals([],[]).
  232.     sort_literals([L|Ls1],Ls2) :-
  233.       sort_literals(Ls1,Ls3),
  234.       sort_literals_1(L,Ls3,Ls2),
  235.       !.
  236.     sort_literals_1(L1,[L2|Ls1],[L2|Ls2]) :-
  237.       sort_literals_2(L1,L2),
  238.       !,
  239.       sort_literals_1(L1,Ls1,Ls2).
  240.     sort_literals_1(L,Ls,[L|Ls]).
  241.     sort_literals_2(not L1,not L2) :-
  242.       !,
  243.       order_term(L1,>,L2),
  244.       !.
  245.     sort_literals_2(not L1,L2) :- !.
  246.     sort_literals_2(L1,not L2) :-
  247.       !,
  248.       fail.
  249.     sort_literals_2(L1,L2) :-
  250.       !,
  251.       order_term(L1,>,L2),
  252.       !.
  253.  
  254. %%%    
  255. %%% Assert the equality axioms.
  256. %%%
  257.     assert_eq_axioms(N,N) :-
  258.       not(equality_transform),
  259.       !.
  260.     assert_eq_axioms(N1,N2) :-
  261.       semi_internal_form([X=X],C1),
  262.       assertz(sent_C(C1)),
  263.       semi_internal_form([Y=Z,not X=Y,not X=Z],C2),
  264.       assertz(sent_C(C2)),
  265.       write_line(5,'equality axioms:'),
  266.       write_line(10,'[X=X]'),
  267.       write_line(10,'[Y=Z,not X=Y,not X=Z]'),
  268.       N2 is N1+2,
  269.       !.
  270.  
  271. %%%
  272. %%% Print_eq_trans prints an equality transformation.
  273. %%%
  274.     print_eq_trans(_,_) :-
  275.       not(outtreq),
  276.       !.
  277.     print_eq_trans(C1,C2) :-
  278.       write_line(10,'equality transformation:'),
  279.       not(not(print_eq_orig(C1))),
  280.       not(not(print_eq_trans(C2))),
  281.       !.
  282.     print_eq_orig(C) :-
  283.       vars_tail(C,V),
  284.       var_list(V),
  285.       write_line(13,'orig:  ',C),
  286.       !.
  287.     print_eq_trans(C) :-
  288.       vars_tail(C,V),
  289.       var_list(V),
  290.       write_line(13,'trans: ',C),
  291.       !.
  292.  
  293. %%%
  294. %%% Transform_equations_round asserts the transformed equations at the
  295. %%% beginning of a round.
  296. %%%
  297.     transform_equations_round :-
  298.       equality_transform,
  299.       equality_transform_by_round,
  300.       !,
  301.       cputime(TT1),
  302.       transform_equations_round_1,
  303.       split_clauses,
  304.       cputime(TT2),
  305.       TT3 is TT2 - TT1,
  306.       write_line(5,'Equation transform(s): ',TT3),
  307.       !.
  308.     transform_equations_round.
  309.     transform_equations_round_1 :-
  310.       sent_C(cl(_,_,by([S=T],V1a,V1a,_,_),_,sp(S1,_,_),_,_,_,_)),
  311.       eq_trans([S=T],C1),
  312.       vars_tail(C1,V),
  313.       clause_size(C1,CSize),
  314.       not(duplicate_clause_C(CSize,C1,V)),
  315.       !,
  316.       linearize_term(C1,C2,V1,V2),
  317.       vars_literals(C1,W),
  318.       compute_V_lits(W,0,NLits),
  319.       set_sr_status(S1,C2,Sp,Ds),
  320.       list_of_Ns(C2,0,Dis),
  321.       calculate_priority_clause(C2,Sp,Ds,Pr),
  322.       transform_equations_round_2(Pr),
  323.       assertz(sent_C(cl(CSize,NLits,by(C2,V1,V2,V,W),0,Sp,Ds,0,Dis,Pr))),
  324.       fail.
  325.     transform_equations_round_1.
  326.     transform_equations_round_2(Pr) :-
  327.       priority_bound(PrioBound),
  328.       !,
  329.       check_prioritybound(Pr,PrioBound),
  330.       !.
  331.     transform_equations_round_2(_).
  332.